﻿Аксиомы алгебра программ
admin|2009/01/18 18:14:38
##PAGE##
{TOC}

==Основные понятия==
  Эти законы нельзя доказать пользуясь только средствами алгебры
программ, они доказываются в исчислении при помощи свойств
соответствующих комбинирующих форм. Поэтому в алгебере они
принимаются за аксиомы. Так, аксиома <math>[f,g]\circ h = [f\circ h,
g\circ h]</math>, означающая, что для любых функций f,g,h программа слева
равна программе справа, в исчислении соответствует равенству
<math>[(f,g]\circ h:):x = ([f\circ h, g\circ h]):x</math> верному для любых
f,g,h,x. Приведем доказательство этого равенства:

'''Доказательство'''

<math>([f,g]\circ h):x&= [f, g]:h:x </math>  ''по определению композиции''

<math>= \langle f:(h:x), g:(h:x) \rangle</math>  ''по определению     конструкции''

<math>= \langle (f\circ h):x, (g\circ h):x\rangle  </math> ''по определению композиции''

<math>=([f\circ h, g\circ h]):x </math>    ''по определению конструкции''

 Области действия некоторых законов уже, чем область всех объектов.
В частности <math>1\circ [f, g]=f</math> не верно для таких объектов ''x'',
что <math>g:x=\bot</math>. Мы записываем <math>\bar{T}\circ g
\rightarrow\rightarrow 1\circ [f, g]=f</math> для того чтобы указать, что
закон или теорема справа справедлива для таких объектов ''x'',
для который выполнено условие определенности функции g
(<math>\bar{T}\circ g=T</math>), поскольку <math>\bar{T}\circ g:x = T \textrm{,if
} g:x\neq\bot</math>.

 В общем случае мы будем записывать ограниченный закон <math>p\rightarrow\rightarrow f=g</math>
который означает, что для любого объекта ''x'', такого что
<math>p:x=T</math>, верно <math>f:x=g:x</math>.

 Каждый из следующих законов требует, чтобы выполнялось соответствующее утверждение.
Интересующийся читатель легко найдет большинство доказательств таких
утверждений (два из них приведены ниже). Определим сначала обычное
упорядочение функций и эквивалентность в терминах этого
упорядочения:

'''Определение''', <math>f \leq g</math> тогда н только тогда, когда для всех
объектов ''х'' либо ''f:х= ''<math>\bot</math>, либо ''f:x=g:x''

'''Определение.'''<math>f=g</math> тогда и только тогда, когда <math>f \leq g</math> и
<math>g \leq f</math>. Легко убедиться в том, что <math>\leq</math>  является частичным
упорядочением; <math>f \leq g</math> означает, что ''g'' является обобщением
для ''f'',  а <math>f=g</math> тогда и только тогда, когда <math>f:x=g:x</math> для
всяких объектов ''х''. Приведем теперь список алгебраических
законов, перечисляемых по парам основных функциональных форм.

==Список аксиом алгебры программ==
===Композиция и конструкция===


=====I.1=====
 <math>[f_1,\ldots,f_n]\circ g = [f_1\circ g,\ldots, f_n\circ g]</math>

=====I.2=====
 <math>\alpha f\circ[g_1,\ldots,g_n]=[f\circ g_1,\ldots,f\circ g_n]</math>

=====I.3===== 
<math>/f\circ[g_1,\ldots,g_n]=f\circ[g_1,/f\circ[g_2,\ldots,g_n]]</math> при n>= 2

=====I.4===== 
<math>f\circ[\bar{x},g]=(bu f x)\circ g</math>

=====I.5=====
<math>s\circ [f_1,\ldots,f_n]\leq f_s</math> для любого селектора ''s'', ''s'' >= 2

=====I.5.1=====
<math>[f_1\circ 1,\ldots,f_n\circ n]\circ[g_1,\ldots,g_n]=[f_1\circ g_1,\ldots,f_n\circ g_n]</math>

=====I.6===== 
<math>tl\circ[f_1]\leq\emptyset\textrm{ и } tl\circ[f_1,\ldots,f_n]\leq[f_2,\ldots,f_n]</math> при n >=  2

                   <math>\bar{T}\circ f\rightarrow\rightarrow tl\circ[f_1]=\emptyset</math> и <math> tl\circ[f_1,\ldots,f_n]=[f_2,\ldots,f_n]</math>  при n>= 2

=====I.7===== 
<math>distl\circ[f, [g_1,\ldots,g_n]]=[[f,g_1],\ldots,[f,g_n]]</math>


                   <math>\bar{T}\circ f\rightarrow\rightarrow distl\circ[f, \emptyset]=\emptyset</math>

                   Аналогичный закон справедлив для дистрибутивности справа.

=====I.8===== 
<math>apndl\circ[f,[g_1,\ldots,g_n]]=[]f,g_1,\ldots, g_n</math>

                   <math>null\circ g\rightarrow\rightarrow apndl\circ[f,g]=f</math>

=====I.9=====
 <math>[\ldots,\bar{\bot},\ldots]=\bar{\bot}</math>

=====I.10===== 
<math>apndl\circ[f\circ g, \alpha f\circ h]=\alpha f \circ apndl\circ[g,h]</math>

=====I.11===== 
<math>pair\&not\circ null\circ 1\rightarrow\rightarrow apndl\circ[[1\circ1,2],distr\circ[tl\circ 1,2]]=distr</math>

                     где <math>f \& g = and\circ[f,g] \textrm{; } pair=atom\longrightarrow\bar{F};eq\circ[length, \bar{2}] </math>

                     (аналогично для левой свертки)

===Композиция и условие===
Ассоциирующиеся скобки справа опущены.

=====II.1=====
 <math>(p\rightarrow f;g)\circ h=p\circ h\rightarrow f\circ h;g\circ h</math>

=====II.2===== 
<math>h\circ(p\rightarrow f;g)=p\rightarrow h\circ f;h\circ g</math>

=====II.3===== 
<math>or\circ[q, not\circ q]\rightarrow\rightarrow and\circ[p,q]\rightarrow f</math>;

                   <math>and\circ[p,not\circ q]\rightarrow g;h=p\rightarrow(q\rightarrow f;g);\ h</math>

=====II.4 =====
<math>p\rightarrow(p\rightarrow f;g);h=p\rightarrow f; h</math>


===Композиция и другие===
=====III.1=====
 <math>\bar{x}\circ f\leq \bar{x}</math>

                     <math>\bar{T}\circ f \rightarrow\rightarrow \bar{x}\circ f=\bar{x}</math>

=====III.1.1===== 
<math>\bar{\bot}\circ f=f\circ\bar{\bot}=\bar{\bot}</math>

=====III.2=====
 <math>f\circ id=id\circ f= f</math>

=====III.3===== 
<math>pair\rightarrow\rightarrow1\circ distr=[1\circ1,2]</math> также

                     <math>pair\rightarrow\rightarrow1\circ t =2</math> и т.д

=====III.4=====
 <math>\alpha(f\circ g)=\alpha f\circ \alpha g</math>

=====III.5=====
 <math>null\circ g \rightarrow\rightarrow\alpha f\circ g =\emptyset</math>


===Условие и конструкция===
=====IV.1===== 
<math>[f_1,\ldots.(p\rightarrow g ;h),\ldots,f_n]=</math>

                     <math>p\rightarrow[f_1,\ldots,g,\ldots,f_n];[f_1,\ldots,h,\ldots,f_n]</math>

=====IV.1.1=====
 <math>[f_1,\ldots.(p_1\rightarrow g_1,\ldots,p_n\rightarrow g_n ;h),\ldots,f_m]=</math>

                       <math>p_1\rightarrow[f_1,\ldots,g_1,\ldots,f_m];</math>

                       <math>\ldots;p_n\rightarrow[f_1,\ldots,g_n,\ldots,f_m];[f_1,\ldots,h,\ldots,f_m]</math>

===Условие===
=====V.1===== <math>p\rightarrow(q\rightarrow r; s);(t\rightarrow u;v)=(p\rightarrow q;t)\rightarrow(p\rightarrow r; u);(p\rightarrow s; v)</math>


==Пример доказательства двух аксиом по семантике программы==
 Мы приводим доказательства
справедливости утверждения для законов '''I.10''' и '''I.11''',
которые немного сложнее, чем большинство остальных.

===Аксиома I.10===
<math>apndl\circ[f\circ g, \alpha f\circ h]=\alpha f \circ
 apndl\circ[g,h]]</math>

''Доказательство.'' Мы покажем, что для любого объекта ''x''
обе указанные выше функции порождают одинаковые результаты.

''Случай 1''. <math>h:x</math> - это не последовательность и не <math>\emptyset</math>.
Тогда обе части при применении к ''x'' порождают <math>\bot</math>.

''Случай 2.'' <math>h:x=\emptyset</math>. Тогда

<math>
 apndl\circ[f\circ g,\alpha f\circ h]:x\\
 = apndl:\langle f\circ g:x,\emptyset\rangle=\langle f:(g:x)\rangle\\
 \alpha f \circ apndl\circ[g,h]&=\alpha f\circ apndl:\langle g:x, \emptyset\rangle=\alpha f\circ apndl:\langle g:x\rangle\\
 =\langle f:(g:x)\rangle
</math>

''Случай 3.'' <math>h:x=\langle y_1,\ldots, y_n\rangle</math>.Тогда

<math>
  apndl\circ[f\circ g,\alpha f\circ h]:x &= apndl:\langle f\circ g:x,\alpha f:\langle y_1,\ldots, y_n\rangle\rangle\\
                                         &= \langle f:(g:x),f:y_1,\dots,f:y_n\rangle\\
        \alpha f \circ apndl\circ[g,h]:x &= \alpha f \circ apndl:\langle g:x,\langle y_1,\ldots, y_n\rangle\rangle\\
                                         &= \alpha f :\langle g:x,y_1,\ldots, y_n\rangle\\
                                         &= \langle f:(g:x),f:y_1,\dots,f:y_n\rangle
</math>

===Аксиома I.11===.
<math>pair\&not\circ null\circ 1\rightarrow\rightarrow apndl\circ[[1\circ1,2],distr\circ[tl\circ 1,2]]=distr</math>

''Доказательство.'' Мы покажем, что для любой пары <math>\langle x,y\rangle</math>,
где <math>x\neq\emptyset</math>, согласно сформулированному ограничению, обе указанные выше функции порождают одинаковые результаты.

''Случай 1.'' ''x'' является атомом или <math>\bot</math>. Тогда <math>distr:\langle x,y\rangle=\bot</math>, потому что <math>x\neq\emptyset</math>.
Левая часть также порождает <math>\bot</math>, поскольку <math>tl\circ1:\langle x,y \rangle=\bot</math> и все функции сохраняют <math>\bot</math>.

''Случай 2.'' <math>x=\langle x_1,\ldots,x_n\rangle</math>. Тогда

<math>
apndl\circ[[1\circ1,2],distr\circ[tl\circ 1,2]]:\langle x,y\rangle \\
    =apndl:\langle\langle1:x,y\rangle, distr:\langle tl:x,y\rangle\rangle\\
    =apndl:\langle\langle x_1,y\rangle,\emptyset\rangle=\langle\langle x_1, y\rangle\rangle \textrm{ если }tl:x=\emptyset\\
    =apndl:\langle\langle x_1,y\rangle,\langle\langle x_2,y\rangle, \ldots,\langle x_n,y\rangle \rangle\rangle \textrm{ если }tl:x\neq\emptyset\\
    =\langle\langle x_1,y\rangle,\ldots,\langle x_n,y\rangle\rangle\\
    =distr:<x,y>
</math>

==Пример доказательства эквивалентности программ==
 В качестве примера использования вышеприведенных законов докажем
эквивалентность двух программ умножения матриц. 

Рассмотрим программуv1:

 <math>Def MM = \alpha\alpha IP\circ \alpha distr\circ distl\circ[1, trans \circ 2] </math> 


которая перемножает пару матриц.
 
Докажем, что ее начальный сегмент MM', где

<math>Def MM' = \alpha\alpha IP\circ \alpha distr\circ distl</math>

 который перемножает пару матриц, после того как одна из них
была транспонирована, может быть описан рекурсивно. 

Иначе говоря,покажем, что MM' удовлетворяет следующему уравнению, рекурсивно
описывающему ту же функцию(на парах):
<math>f=null\circ1\rightarrow\emptyset; apndl\circ[\alpha IP\circ distl\circ[1\circ1,2], MM'\circ[tl\circ1,2]]</math>

Наше доказательство примет форму демонстрации того, что следующая
функция R, где
<math>Def R=null\circ1\rightarrow\emptyset; apndl\circ[\alpha IP\circ distl\circ[1\circ1,2], MM'\circ[tl\circ1,2]]</math>
при любых парах <math>\langle x,y\rangle</math> эквивалентна функции MM'.
Функция R ''умножает'' две матрицы, когда первая содержит более чем
0 строк; вычисляется первая строка ''произведения'' (при помощи
<math>[\alpha IP\circ distl\circ[1\circ1,2]</math>) и присоединяется к
''произведению'' остатка первой матрицы и второй матрицы.


===Теорема===
<math>pair\rightarrow\rightarrow MM'=R</math>,

где

<math>Def MM' = \alpha\alpha IP\circ \alpha\ distr\circ distl</math>

<math>Def R=null\circ1\rightarrow\emptyset; apndl\circ[\alpha IP\circ distl\circ[1\circ1,2], MM'\circ[tl\circ1,2]]</math>

=====Случай 1=====<math>pair\&null\circ1\rightarrow\rightarrow
MM'=R</math>

<math>pair\&null\circ1\rightarrow\rightarrow R=\emptyset</math>
по определению R

<math>pair\&null\circ1\rightarrow\rightarrow MM'=\emptyset</math>

так как <math>distr:\langle\emptyset, x\rangle=\emptyset</math> по определению
distr
и <math>\alpha f:\emptyset=\emptyset</math> по определению ""Применить ко
всем"".\\
Таким образом <math>\alpha\alpha IP\circ \alpha\ distr\circ
distl:\langle\emptyset, x\rangle = \emptyset</math>.

Поэтому <math>pair\&null\circ1\rightarrow\rightarrow
MM'=R</math>

=====Случай 2.=====<math>pair\&not\circ null\circ1\rightarrow\rightarrow MM'=R</math>


<math>
pair\&not\circ null\circ1\rightarrow\rightarrow R=R'</math> по
определению R и R', где

<math>R'=apndl\circ[\alpha IP\circ distl\circ[1\circ1,2], MM\circ[tl\circ1,2]]</math>
Заметим, что
<math>R'=apndl\circ[f\circ g,\alpha f\circ h]</math>
где
<math>
f&=\alpha IP\circ distl\\
g&=[1\circ1.2]\\
h&=distr\circ[tl\circ1,2]\\
\alpha f &= \alpha(\alpha IP\circ distl)=\alpha\alpha IP\circ \alpha
distl 
</math>(согласно [Axioms#IIIE_19|III.4]).

Таким образом, согласно [Axioms#IBA_9|I.10],
<math>
R'=\alpha f\circ apndl\circ[g,h].
</math>
 Теперь <math>apndl\circ[g,h]=apndl\circ[[1\circ1, 2],
distr\circ[tl\circ 1,2]]</math>, поэтому в силу [Axioms#IBB_10|I.11]
<math>pair\&not\circ null\circ1\rightarrow\rightarrow
apndl\circ[g,h]=distr.
</math>

Итак, согласно равенствам выше,
<math>
pair\&not\circ null\circ1\rightarrow\rightarrow R&=R'
                                                 &=\alpha f\circ distr=\alpha\alpha IP\circ\alpha distl\circ distr=MM'
</math>
Случаи 1 и 2, взятые вместе доказывают теорему.



